FDL - Step of Proof: fseg_member

Step of Proof: fseg_member

Inference at *
Iof proof for Lemma fseg member:

T:Type, l1, l2:(T List), x:T. fseg(T;l1;l2)

(x

l1)

(x

l2)

by ((((Auto

)

CollapseTHEN (D (-2)

))

)

CollapseTHEN (((((((if (first_bool T:b

C) then HypSubst' else RevHypSubst') ( -2)( 0))

)

CollapseTHENA (Auto

))

)

CollapseTHEN (((((

CRWO "member_append" 0)
THENM (OrRight))

)
TCollapseTHEN (Auto

))

))

))

TC.

Definitions fseg(T;L1;L2), x:A. B(x), ||as||, i j , A B, [car / cdr], SQType(T), type List, s ~ t, , {x:A| B(x)} , s = t, t T, , Type, x:A. B(x), P Q, P & Q, x:A B(x), P Q, P Q, x:AB(x), P Q, (x l), {T}

Lemmas fseg wf, non neg length, cons one one, guard wf, nat wf, member wf, member append, l member wf